Nuprl Lemma : divides_anti_sym_n 11,40

a,b:. divides(ab divides(ba (a = b  
latex


Definitionst  T, P  Q, x:AB(x), prop{i:l}, , , P  Q, decidable(P), x:AB(x), divides(ba), False, A, A  B
Lemmasnat wf, divides wf, decidable int equal, divisors bound

origin